import Mathlib

namespace CNVSProbabilisticCore

structure ThresholdModel where
  k : ℕ
  usefulCompromised : Fin k → Nat
  r : Nat

def X (M : ThresholdModel) : Nat :=
  Finset.univ.sum M.usefulCompromised

def RecStar (M : ThresholdModel) : Prop :=
  M.r ≤ X M

theorem recstar_iff_threshold (M : ThresholdModel) :
    RecStar M ↔ M.r ≤ X M := by
  rfl

theorem no_reconstruction_below_threshold
    (M : ThresholdModel)
    (h : X M < M.r) :
    ¬ RecStar M := by
  intro hRec
  exact Nat.not_lt_of_ge hRec h

theorem reconstruction_at_or_above_threshold
    (M : ThresholdModel)
    (h : M.r ≤ X M) :
    RecStar M := by
  exact h

def PositiveExample : ThresholdModel where
  k := 3
  usefulCompromised := fun i =>
    if i = 0 then 1 else if i = 1 then 1 else 0
  r := 2

example :
    X PositiveExample = 2 := by
  native_decide

example :
    RecStar PositiveExample := by
  unfold RecStar
  change 2 ≤ X PositiveExample
  rw [show X PositiveExample = 2 by native_decide]

def NegativeExample : ThresholdModel where
  k := 3
  usefulCompromised := fun i =>
    if i = 0 then 1 else 0
  r := 2

example :
    X NegativeExample = 1 := by
  native_decide

example :
    ¬ RecStar NegativeExample := by
  unfold RecStar
  change ¬ 2 ≤ X NegativeExample
  rw [show X NegativeExample = 1 by native_decide]
  norm_num

end CNVSProbabilisticCore